\documentclass[11pt,a4paper]{scrartcl}
\usepackage[ngerman]{babel}
\usepackage{palatino}
\setkomafont{section}{\normalfont\bfseries\Large}
\setkomafont{subsection}{\normalfont\bfseries\large}
\setkomafont{subsubsection}{\normalfont\bfseries\normalsize}
\setkomafont{paragraph}{\normalfont\bfseries\normalsize}
\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{nicefrac}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{url}

\parindent0pt 
\parskip4pt

\usepackage[left=2.5cm,right=2.5cm,top=2cm,bottom=2.5cm]{geometry}

\usepackage{tikz}
\usetikzlibrary{trees,decorations,arrows,automata,shadows,positioning,plotmarks,shapes}
\newcommand{\svs}{\emph{SVS }}

\usepackage{listings}

\begin{document}
\thispagestyle{empty}
\setcounter{page}{1}
\Large\textbf{Softwarequalitätsmanagement im ASE}\hfill \normalsize \today

\Large \textbf{Model-Checking von Stateflow Modellen} \normalsize \hfill Peuser, Jungnickel, Brodmann 

\hrule


\section*{Computation Tree Logic (CTL)}
\vspace*{-0.4cm}
\paragraph{CTL-Syntax} Formeln in CTL haben folgenden Aufbau
\begin{eqnarray}
 \varphi &::=& \top \mid \bot \mid p \mid \lnot \varphi \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \varphi \Rightarrow \varphi \mid \varphi \Leftrightarrow \varphi      \nonumber \\
   & & \mathsf{AX} \; \varphi \mid \mathsf{EX} \; \varphi \mid \mathsf{AF} \; \varphi \mid \mathsf{EF} \; \varphi \mid \mathsf{AG} \; \varphi \mid \mathsf{EG} \; \varphi \nonumber \\
    & & \mathsf{A} \; [\varphi \mathop{\mathsf{U}} \varphi] \mid \mathsf{E} \; [\varphi \mathop{\mathsf{U}} \varphi] \nonumber
\end{eqnarray}

\paragraph{CTL-Semantik} Die Bedeutung von Formeln in CTL ist wie folgt definiert:

	\begin{minipage}[c]{0.6\textwidth} 
	Pfadquantoren:
\begin{itemize}
\itemsep0pt
\item $\mathsf{A}$ : Auf allen folgenden Pfaden
\item $\mathsf{E}$ : Auf mindestens einem Pfad
\end{itemize}
Temporaloperatoren:
\begin{itemize}
\itemsep0pt
\item $\mathsf{X} \; \varphi$ : Im nächsten Zustand gilt $\varphi$
\item $\mathsf{F} \; \varphi$ : In einem folgenden Zustand gilt $\varphi$
\item $\mathsf{G} \; \varphi$ : In allen folgenden Zuständen gilt $\varphi$
\item $\left[ \varphi \mathop{\mathsf{U}} \psi \right]$ : Es gilt $\varphi$ bis zum ersten Auftreten von $\psi$
\end{itemize}
	\end{minipage}
	\hfill
	\begin{minipage}[c]{0.3\textwidth}
	\begin{center}
	\begin{tikzpicture}[auto]
	\node  (a) at (-0.5,0) {\Huge $\mathsf{Q}$};
	\node  (b) at (.5,0.03) {\Huge $\mathsf{T}$};
	\node  (c) at (-.5,1) {\small Pfadquantor};
	\node  (d) at (.5,-1) {\small Temporaloperator};

	%\draw (a) [->,thick] to node {} (c);
	%\draw (b) [->,thick] to node {} (c);
	\draw (c) [->,thick] to node {} (a);
	\draw (d) [->,thick] to node {} (b);
	%\draw (d) [->,bend left,dashed,color=red] to node {} (a);
		
	\end{tikzpicture}
 	\end{center}
	\end{minipage}
\paragraph{Gültigkeit} 
Erfüllt eine Systembeschreibung $\mathcal{M}$ in einem Zustand $\mathsf{S}$ eine CTL Formel $\varphi$, so schreiben wir: $$\mathcal{M},\mathsf{S} \vDash \varphi$$

Ist $\mathsf{S}$ ein initialer Zustand, schreiben wir: $$\mathcal{M} \vDash \varphi$$
\section*{Model-Checking von Statflow Modellen}
\vspace*{-0.4cm}
\paragraph{Hauptproblem 1: Zustandsexplosion} 
Werden Eingangsvariablen mit einem großen (potentiell unendlichen) Datenbereich verwendet, entstehen exponentiell viele (und potentiell unendlich viele) Zustände für das System. \emph{Model-Checker} sind in der Regel nicht in der Lage auf unendlichen Zustandsräumen die Korrektheit einer Spezifikation zu prüfen. Eine Lösung für dieses Problem ist die \emph{eigenschaftserhaltende} Abstraktion von Variablen auf einen kleinen, endichen Datenbereich.

\paragraph{Eigenschaftserhaltend} Eigenschaftserhaltend bedeutet, dass aus der Gültigkeit einer CTL-Formel ($\texttt{Abs}\varphi$) im abstrakten Modell ($\texttt{Abs}\mathcal{M}$) immer die Gültigkeit der CTL-Formel ($\varphi$) im konkreten Modell ($\mathcal{M}$) abgeleitet werden kann: $$(\texttt{Abs}\mathcal{M} \vDash \texttt{Abs}\varphi) \Rightarrow (\mathcal{M} \vDash \varphi)$$

\paragraph{Hauptproblem 2: Hierachische Zustandssysteme}
Von den meisten \emph{Model-Checkern} werden hierarchische Zustandssysteme nicht unterstützt. Ein hierarchischer Aufbau dient primär der Übersichtlichkeit.\\
Um das Modell zu überprüfen muss dieses erst in eine flache Struktur überführt werden.


\end{document}
